Skip to content

Strict order equational reasoning #1203

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 2 commits into from
May 19, 2025
Merged

Strict order equational reasoning #1203

merged 2 commits into from
May 19, 2025

Conversation

LorenzoMolena
Copy link
Contributor

@LorenzoMolena LorenzoMolena commented Apr 18, 2025 •
edited
Loading

Facilities for equational reasoning involving mixed use of <, ≤, ≡ in a type that is both a quoset and a poset (with the additional data of <-≤-trans, ≤-<-trans ) to obtain a strict inequality (having at least a < in the chain).
This is inspired from Relation.Binary.Reasoning.PartialOrder of the Agda Standard Library.

Some notes:

  • Compatibility with the existing equational reasoning already present in Prelude can be achieved with a nested chain of equations, as shown in the commented example.
    Such a chain can be written without nested equations, but it is not recomended, since it will perform a bunch of substs, and the combinators from Prelude (such as _ ≡[ i ]⟨ p i ⟩ _ ) cannot be used.
  • begin is needed at the start of the chain, since it has to extract a strict inequality from the given chain.
  • It should be easy to expand the code to also extract nonstrict inequalities, in that case a < won't be required in the chain.

LorenzoMolena and others added 2 commits April 18, 2025 17:16
@LorenzoMolena @hexwell
Add QuosetReasoning.agda
c2717bb 
Co-authored-by: Ettore Forigo <ettore.forigo@gmail.com>
@LorenzoMolena
add missing no-eta-equality in SubRelation, make SubRelation instan…
ac71060 
…ce private
@felixwellen felixwellen merged commit 2738401 into agda:master May 19, 2025
1 check passed
marcinjangrzybowski added a commit to marcinjangrzybowski/cubical that referenced this pull request Jun 26, 2025
@marcinjangrzybowski
Squashed commit of the following:
18f8334 
commit d08dabfacb486fb77a2ded077a3f0593968412e8
Author: Marcin Jan Turek-Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Thu Jun 26 22:32:26 2025 +0200

    works

commit 74b6ee0df2aaba26be3f09f81b2020470b27cc44
Author: Marcin Jan Turek-Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Thu Jun 26 22:29:59 2025 +0200

    gi

commit f89d4d7f172ae7da24a385efdd783209a5b2bdea
Author: Marcin Jan Turek-Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Thu Jun 26 22:29:15 2025 +0200

    gi

commit 3528c1128f48573748c240b3b5d3ea27fee5e0e5
Author: Marcin Jan Turek-Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Thu Jun 26 20:04:00 2025 +0200

    cleanup

commit 4028c0010c1f0f48f54577ce418185648b2b9902
Author: Marcin Jan Turek-Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Thu Jun 26 20:02:46 2025 +0200

    cleanup

commit 02f1aa892a739e61be52f2a609d0bd5891133639
Merge: 07914eea ac62dd4
Author: Marcin Jan Turek-Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Thu Jun 26 19:09:38 2025 +0200

    pre-merge

commit 07914eeae43b77109983039e6d2e6c67fbae3f2f
Author: Marcin Jan Turek-Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Thu Jun 26 18:59:53 2025 +0200

    integration done

commit ac62dd4
Author: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date:   Wed Jun 25 17:16:13 2025 +0530

    Add Rezk Completion by HIT (agda#1188)

    * Add Rezk Completion by HIT

    * Update Construction.agda

    * Removed trailing whitespaces

    * Remove trailing whitespace

    * Replace HIT with GroupoidQuotient

    * shorter proof of `inc-surj`

    * fix whitespace

    * Forgot to import GroupoidQuotients

    * add implicit argument

commit b15ec4e
Author: Marcin Jan Turek-Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Tue Jun 24 06:45:56 2025 +0200

    wip

commit 55479ef
Author: Marcin Jan Turek-Grzybowski <marcin@Marcins-MacBook-Pro.local>
Date:   Wed May 28 16:00:42 2025 +0200

    wip - dirty

commit ecf1bbb
Author: Laine Taffin Altman <alexanderaltman@me.com>
Date:   Fri May 23 03:17:16 2025 -0700

    Fix makefile race condition (agda#1210)

    If you use `make -j gen-everythings listings`, currently there is a near-certainty that the `listings` task will fail because the Everythings modules haven't been generated yet.  This PR enforces the dependency.

commit 43183c8
Author: michael <1700346+mzhang28@users.noreply.github.com>
Date:   Thu May 22 17:01:37 2025 -0500

    Five lemma (agda#1166)

    * exact sequences

    * complete five proof

    * make five safe

    * fix newline

    * exactness over a successor structure

    * working again

    * fix whitespace...

    * clean up, just five

    * clean up

    * make implicit + rename isExact so the names are more descriptive

    * fix whitespace

commit 63d187d
Author: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date:   Tue May 20 22:52:24 2025 +0530

    Formalize Theorem 7.2.2 in the HoTT Book (agda#1180)

    * Formalize Theorem 7.2.2 in the HoTT Book

    * move Theorem 7.2.2 to Cubical.Relation.Binary.Properties

    * Remove a few extra spaces

    This is not really necessary but it looks better

commit 06e62f4
Author: michael <1700346+mzhang28@users.noreply.github.com>
Date:   Tue May 20 07:24:54 2025 -0500

    Composition of left module homomorphisms (agda#1176)

    * implement composition of left module homomorphisms

    * pull out to top level

    * fix whitespace

commit 78203ee
Author: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date:   Mon May 19 21:41:29 2025 +0530

    Remove duplicated lemma (agda#1189)

    * Remove duplicated lemma

    agda#1017

    * Insert brackets

commit 2738401
Author: LorenzoMolena <164308953+LorenzoMolena@users.noreply.github.com>
Date:   Mon May 19 17:52:30 2025 +0200

    Strict order equational reasoning (agda#1203)

    * Add QuosetReasoning.agda

    Co-authored-by: Ettore Forigo <ettore.forigo@gmail.com>

    * add missing `no-eta-equality` in SubRelation, make SubRelation instance private

    ---------

    Co-authored-by: Ettore Forigo <ettore.forigo@gmail.com>

commit 69b70a2
Author: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date:   Mon May 19 21:19:57 2025 +0530

    Add inducedFun for EM1 (agda#1208)

    * Add files via upload

    * Delete Base.agda

    No idea what this file is doing here

    * Delete Properties.agda

    Must have accidentally put this here when I was editing dagger-cat

    * Add inducedFun for EM1

commit 22458b7
Author: LeeeeT <me@LeeeeT.dev>
Date:   Mon May 19 18:46:33 2025 +0300

    Add missing minus symbol (agda#1207)

commit 3291fc1
Author: Felix Cherubini <felix.cherubini@posteo.de>
Date:   Mon May 19 17:24:35 2025 +0200

    Release for agda 2.7 (agda#1206)

    * test new ci script

    * fix

    * use fix-whitespace action

    * blindly try stuff

    * blindly try stuff

    * blindly try stuff

    * untabify...

    * Revert "blindly try stuff"

    This reverts commit 6fe71f3.

    # Conflicts:
    #	.github/workflows/ci-ubuntu.yml

    * use fix-whitespace action

    * whitespace

    * whitespace

    * fix

    * fix

    * fix

    * fix

    * Fix path of fix-whitespace

    * Remove unnecessary step to generate user-manual.pdf

    * Bump base in cubical-utils.cabal

    * bump version number everywhere, update README and RELEASE

    * trailing newline needed?

    * update flake

    ---------

    Co-authored-by: Andreas Abel <andreas.abel@ifi.lmu.de>
    Co-authored-by: Naïm Favier <n@monade.li>

commit eef2ed6
Author: Marcin Jan Turek-Grzybowski <marcin@Marcins-MacBook-Pro.local>
Date:   Thu May 15 07:17:58 2025 +0200

    wip

commit 71f32f0
Author: Andreas Abel <andreas.abel@ifi.lmu.de>
Date:   Fri May 9 21:51:25 2025 +0200

    Prep for Agda 2.8.0: remove some spurious `private`

commit d5b7bce
Author: Marcin Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Mon Apr 21 20:46:48 2025 +0200

    sync

commit 35d2919
Merge: 385066b cb0510c
Author: Evan Cavallo <evanc@chalmers.se>
Date:   Fri Mar 21 06:08:36 2025 +0100

    Merge pull request agda#1157 from Trebor-Huang/devalapurkar-haine

    Devalapurkar & Haine

commit cb0510c
Author: ecavallo <evancavallo@gmail.com>
Date:   Thu Mar 20 18:40:56 2025 +0100

    cosmetic changes

commit 52cf2a1
Author: ecavallo <evancavallo@gmail.com>
Date:   Thu Mar 20 18:40:42 2025 +0100

    more informative type signatures

commit 01c36f4
Author: ecavallo <evancavallo@gmail.com>
Date:   Thu Mar 20 18:40:23 2025 +0100

    prefer copattern matching to record syntax

commit fa0eba6
Author: ecavallo <evancavallo@gmail.com>
Date:   Thu Mar 20 13:59:26 2025 +0100

    make pushout to wedge equivalence opaque

commit 4155afd
Merge: 01fa420 385066b
Author: ecavallo <evancavallo@gmail.com>
Date:   Tue Mar 18 14:01:34 2025 +0100

    Merge branch 'master' into devalapurkar-haine

commit 385066b
Author: Loïc Pujet <38562414+loic-p@users.noreply.github.com>
Date:   Tue Mar 4 16:53:03 2025 +0100

    Reduced homology of CW complexes (agda#1175)

    * Reduced homology of CW complexes

    * explicit description of the augmentation map

commit 90c3244
Author: Marcin Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Fri Feb 14 16:53:06 2025 +0100

    wip

commit e8ff0c1
Author: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date:   Fri Feb 14 21:06:39 2025 +0530

    Move `factorial` from `Cubical.Data.Fin.LehmerCode` to `Cubical.Data.Nat.Properties` (agda#1184)

    * Update LehmerCode.agda

    * Update Properties.agda

    add `factorial` here

    * Update LehmerCode.agda

    made it export `factorial` so nothing else in the library that depends on `factorial` being exported breaks

    * Removed dependency on LehmerCode exporting `factorial`

    * Removed dependency on LehmerCode exporting `factorial`

    * Removed dependency on LehmerCode exporting `factorial`

    * Remove the public export of `factorial` from LehmerCode.agda

commit 3d5bb7d
Author: Brad Dragun <35275808+LuuBluum@users.noreply.github.com>
Date:   Tue Feb 11 23:02:11 2025 -0700

    Fix missed rename of StrictPoset to Quoset (agda#1185)

commit c16edad
Author: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date:   Sat Feb 8 21:32:52 2025 +0530

    Remove duplicated factorial function (agda#1183)

    `_!` is defined in `Cubical.Data.Nat.Properties`, `factorial` is defined in `Cubical.Data.Fin.LehmerCode`, and they both have identical definitions.

commit f717d46
Author: Brad Dragun <35275808+LuuBluum@users.noreply.github.com>
Date:   Fri Feb 7 09:27:29 2025 -0700

    Basic Order Theory (agda#1154)

    * Add inverses to monoids/comm monoids

    * Add meets and joins to order properties

    * Rewrite isConnected and rename isStronglyConnected

    * Decidable total and linear orders imply discrete

    * Remove discrete requirement

    * Move decidable->discrete from toset to poset

    * Define binary meets/joins and prove properties

    * The negation of a linear order is a poset

    * Define bounds on a poset

    * Mild refactoring

    Rename preorder to proset; rename strict poset
    to quoset (quasiorder) and add strict orders
    as quasiorders with weak linearity

    * Remove unnecessary constructors

    * Define tight relations

    * Reintroduce constructors

    * Lattice basics

    * Distributive lattices

    * Replace compEquiv usages

    * Total orders are distributive pseudolattices

    * Add pseudolattice assumption to make more useful

    * Mappings on posets

    * Downsets and upsets are preserved

    * Defined complete lattices

    * Duals and closures

    * Embeddings form a complete lattice

    * Dual closures

    * Bicomplete subsets

    * Poset equivalences

    * Galois connections

    * Fix typo

    * Fix whitespace

    * Fix build failures

    * Move PosetDownset to where principalDownsets are

    * Fix build failures

    * Split mappings and subsets

    * Fix whitespace

    * Proofs regarding residuals and involutions

    * Cleaner proof

commit f344485
Author: Marcin Grzybowski <marcinjangrzybowski@gmail.com>
Date:   Thu Jan 30 15:55:08 2025 +0100

    wip

commit 01fa420
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Thu Sep 19 22:16:54 2024 +0800

    safe flags

commit 54a2b1f
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Thu Sep 19 21:42:05 2024 +0800

    Fix whitespace

commit a181af8
Merge: f0d49bc 53e400e
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Thu Sep 19 21:36:50 2024 +0800

    Merge remote-tracking branch 'origin/master' into devalapurkar-haine

commit f0d49bc
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Thu Sep 19 21:27:40 2024 +0800

    James

commit d99570a
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Thu Sep 19 21:10:57 2024 +0800

    Hilton–Milnor

commit c983de7
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Thu Sep 19 20:36:36 2024 +0800

    Splitting of loopspace

commit 08a56c4
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Thu Sep 19 20:21:45 2024 +0800

    Oddly specific sigma lemma

commit 51fa7d0
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Thu Sep 19 20:12:35 2024 +0800

    Remove my version in favor of the other

commit dee0c56
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Sun Aug 18 00:08:50 2024 +0800

    extend commutative squares

commit 98bbb7a
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Sun Aug 18 00:08:43 2024 +0800

    tweak

commit a4b23dd
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Thu Aug 15 17:45:42 2024 +0800

    Rename

commit dac0c0e
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Tue Aug 13 02:07:32 2024 +0800

    Pushout using Unit*

commit f9fc7e3
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Mon Aug 12 13:50:15 2024 +0800

    Use PushoutSquare instead

commit 72a7557
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Mon Aug 12 03:58:36 2024 +0800

    Universes

commit 9d50340
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Mon Aug 12 03:18:06 2024 +0800

    Susp (X∙ ⋀ Y∙) ≡ join X Y

commit 4bc6517
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Mon Aug 12 02:51:38 2024 +0800

    Pushout⋁≃Unit

commit 90f1ca9
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Mon Aug 12 02:50:52 2024 +0800

    Remove redundant definition

commit fa2da1a
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Mon Aug 12 02:50:36 2024 +0800

    projection functions

commit 54038ae
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Mon Aug 12 02:31:37 2024 +0800

    join inclusions are null

commit 313b74e
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Mon Aug 12 00:22:40 2024 +0800

    Use pushout squares for cofibInl-⋁

commit d0a06cd
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Sun Aug 11 21:40:16 2024 +0800

    pushout along identity

commit b4e74c1
Author: Trebor-Huang <treborhuang@foxmail.com>
Date:   Sun Aug 11 21:08:23 2024 +0800

    Susp is Pushout 1 <- X -> 1

commit 5dae632
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Sep 17 01:01:18 2024 +0200

    fixes

commit e13f9ab
Merge: 10aea90 e2370fb
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Sep 16 22:22:28 2024 +0200

    Merge remote-tracking branch 'master/master' into cellular_pointed

commit 10aea90
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jun 4 14:42:34 2024 +0200

    minor

commit 1dff2d5
Merge: 46482af a0b4ba3
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jun 4 14:39:52 2024 +0200

    merge

commit 46482af
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jun 4 14:22:49 2024 +0200

    connected clean

commit 787f34f
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jun 4 14:12:57 2024 +0200

    connected done?

commit 73afa8e
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jun 4 02:59:48 2024 +0200

    cleaning

commit 0cb5678
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jun 4 02:59:42 2024 +0200

    cleaning

commit 6bc3664
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Fri May 31 18:51:51 2024 +0200

    pretty much done

commit e4f4003
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Fri May 31 04:09:48 2024 +0200

    almost

commit c7acbee
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Wed May 29 18:11:46 2024 +0200

    stuff

commit 77623bb
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon May 27 03:16:45 2024 +0200

    wip...

commit dac2fd3
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Thu May 23 18:08:06 2024 +0200

    stuff

commit afe51a4
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Wed May 8 18:20:52 2024 +0200

    p2

commit 87fa4c0
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue May 7 18:15:55 2024 +0200

    done?

commit eb6b12e
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue May 7 10:12:34 2024 +0200

    Pointed

commit 3784dcd
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Thu May 2 11:34:11 2024 +0200

    comments

commit beccacd
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Mar 4 12:03:53 2024 +0100

    ojdå

commit 3e53282
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Mar 4 11:31:38 2024 +0100

    broken code

commit ac5249e
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Mar 4 09:39:57 2024 +0100

    wups

commit 1b005a6
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Mar 4 02:22:00 2024 +0100

    ugh

commit 2d3fe1c
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Mar 4 01:48:45 2024 +0100

    wups

commit b1f9e1d
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Mar 4 01:30:09 2024 +0100

    readme

commit 6e259af
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Mar 4 00:38:02 2024 +0100

    cleanup

commit a3f6a9e
Merge: 6ce70a4 f4745a2 4ba3c8e
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Sun Mar 3 21:13:21 2024 +0100

    merge

commit 4ba3c8e
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Sun Mar 3 20:55:52 2024 +0100

    stuff

commit a3bb47e
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Sun Mar 3 20:48:17 2024 +0100

    done?

commit 53bb0f2
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Sun Mar 3 03:52:29 2024 +0100

    stuff

commit 54c7919
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Fri Mar 1 19:08:20 2024 +0100

    stuff

commit 42d6b77
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Thu Feb 29 15:34:05 2024 +0100

    stuff

commit df55d55
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Thu Feb 29 02:49:34 2024 +0100

    More

commit ae6e813
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Feb 27 00:10:56 2024 +0100

    stuf

commit b694120
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Feb 26 16:42:26 2024 +0100

    stuff

commit ea5fefd
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Sun Feb 25 23:02:26 2024 +0100

    stuff

commit f4745a2
Merge: 1c0396c 227b10b
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Wed Jan 31 10:49:17 2024 +0100

    Merge remote-tracking branch 'origin/master'

commit 9071481
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Wed Jan 31 10:46:56 2024 +0100

    stuff

commit e47bad5
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Wed Jan 24 19:53:25 2024 +0100

    wups

commit f7524eb
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jan 23 19:44:57 2024 +0100

    ugh...

commit b7716a4
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jan 23 19:19:56 2024 +0100

    fixes

commit 7313a31
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jan 23 15:04:18 2024 +0100

    wups

commit 7875e3e
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jan 23 14:51:05 2024 +0100

    wups

commit 74a8521
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jan 23 14:47:14 2024 +0100

    wups

commit 5e8b305
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jan 23 14:17:35 2024 +0100

    done?

commit 74596b5
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Jan 23 03:52:06 2024 +0100

    ..

commit 2b8b5fd
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Jan 22 18:50:46 2024 +0100

    more

commit 2fef4ef
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Jan 22 18:36:10 2024 +0100

    stuff

commit c034578
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Thu Jan 18 17:17:24 2024 +0100

    stuff

commit 9d1915d
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Wed Jan 17 02:53:26 2024 +0100

    fix

commit 227b10b
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Thu Jun 8 09:45:56 2023 +0200

    w

commit 3acc6b8
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Thu Jun 8 09:45:28 2023 +0200

    w

commit ea75092
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Thu Jun 8 09:44:37 2023 +0200

    w

commit 52429ff
Merge: 9341710 814d54b
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Thu Jun 8 09:38:02 2023 +0200

    Merge branch 'newM'

commit 9341710
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Fri Jun 2 15:04:54 2023 +0200

    ganea stuff

commit 17f3fc1
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Apr 24 17:13:52 2023 +0200

    rme

commit aadde33
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Apr 24 17:12:41 2023 +0200

    wups

commit e8244ac
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Apr 24 17:10:45 2023 +0200

    duplicate

commit cc6ced2
Merge: b4b6efb f0ad815
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Mon Apr 24 17:10:10 2023 +0200

    done

commit b4b6efb
Merge: 93d7248 9acdecf
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Feb 1 04:02:50 2022 +0100

    m

commit 93d7248
Author: aljungstrom <axel.ljungstrom@hotmail.com>
Date:   Tue Feb 1 04:00:15 2022 +0100

    t
@hexwell hexwell mentioned this pull request Jul 17, 2025
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@LorenzoMolena @felixwellen